es:ES, T:Type, i:Id, P:(T), Q:(ET).
(x:T. Dec(P(x)))
 (L:(T List).
 (xL. e:E. Q(e,x)  (loc(e) = i  Id))
  (xL. P(x)  (e:E. Q(e,x)))
  (((xL.P(x)))  e'@i.True)
  e'@i.xL. P(x)  (e:E. (e loc e'  & Q(e,x)))) 

latex

Definitions	Dec(P), x(s), ES, False, x:A. B(x), A c B, e loc e' , x(s1,s2), A, (xL.P(x)), e@i.P(e), x. t(x), True, E, Id, loc(e), xL. P(x), (x  l), P  Q, P & Q, P  Q, {T}, P  Q, , x:A. B(x), t  T, P  Q, {i..j}, i  j < k, A  B, l[i], i z j, i <z j, hd(l), i  j , ||as||, (e <loc e'), Trans(T;x,y.E(x;y))
Lemmas	l exists wf, es-le-trans, es-locl wf, es-le-total, length wf1, non neg length, le wf, select member, cons member, l member wf, es-loc wf, Id wf, es-E wf, true wf, existse-at wf, not wf, l exists cons, not functionality wrt iff, implies functionality wrt iff, es-le wf, l all wf, l all nil, false wf, l exists nil, decidable wf, event system wf